\begin{tabbing}
$\forall$\=${\it es}$:event\_system\{i:l\}, $i$,$a$:Id, $p$:finite{-}prob{-}space, ${\it ds}$:fpf(Id; $x$.Type),\+
\\[0ex]$P$:(decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$). @$i$ Precondition for $a$(Outcome($p$)) $P$ discrete state(${\it ds}$) $\in$ prop\{i:l\}
\-
\end{tabbing}